1. Field of the Invention
This invention relates to accelerating automatic test pattern generation (ATPG) and logic synthesis/verification by accelerating the Boolean Satisfiability (SAT) problem. In particular, the invention provides for a configurable computing approach for SAT-solving that can offer substantial speedups (&gt;200.times. in many cases) over traditional software approaches. Since Boolean satisfiability approaches are logical-operation-intensive, the hardware approach can show large advantages by mapping portions of the SAT expressions directly to logic gates, and by harnessing large amounts of parallelism in the evaluation of the logic.
2. Related Work
An FPGA (field programmable gate array) is a known integrated circuit whose functionality can be programmed and changed in software itself. Inasmuch as FPGA's are well known and commercially available (for example, the VIRTUALOGIC SLI EMULATOR from IKOS Systems, Inc.), the details thereof will be omitted for clarity. FPGA's are useful in configurable hardware systems. That is, FPGA's can provide a hardware machine whose functionality can change in response to programming by software.
Configurable hardware systems have been used in different ways. Prior uses of configurable computing have often been directed to applications that are computationally intensive and have uniform data. Prior configurable computing applications therefore generally been characterized in that the programmable logic of the FPGA's typically consists of a large number of parallel data paths and very little control. In other words, configurable computing applications have used only simple control flow.
Boolean SAT is a problem which requires more than simple control flow, and a first configurable hardware system for implementing Boolean SAT was proposed by the same inventors in U.S. patent application Ser. No. 08/919,282, filed on Aug. 28, 1997, incorporated herein by reference in its entirety. This first SAT-solving configurable hardware system featured a SAT solver based generally on the Davis-Putnam algorithm. The basic Davis-Putnam algorithm provides for backtracking that is chronological. That is, the algorithm backtracks to the most recently assigned variable.
The inventors are aware of two other proposals for solving SAT using reconfigurable hardware:
T. Suyama, M. Yokoo, and H. Sawada. Solving Satisfiability Problems on FPGA's. In 6th Int'l Workshop on Field-Programmable Logic and Applications, September 1996. PA1 M. Abramovici and D. Saab. Satisfiability on Reconfigurable Hardware. In Seventh International Workshop on Field Programmable Logic and Applications, September 1997. PA1 P. Goel. An Implicit Enumeration Algorithm to Generate Tests for Combinational Logic Circuits. IEEE Transactions on Computers, C30(3):215-222, March 1981. PA1 T. Larrabee. Test Pattern Generation Using Boolean Satisfiability. In IEEE Transactions on Computer-Aided Design, volume 11, pages 4-15, January 1992. PA1 S. Chakradhar, V. Agrawal, and S. Rothweiler. A transitive closure algorithm for test generation. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 12(7):1015-1028, July 1993. PA1 P. Stephan, R. Brayton, and A. Sangiovanni-Vincentelli. Combinational Test Generation Using Satisfiability. Department of Electrical Engineering and Computer Sciences, University of California at Berkeley, 1992. UCB/ERL Memo M92/112. PA1 J. Silva and K. Sakallah. GRASP-A New Search Algorithm for Satisfiability. In IEEE ACM International Conference on CAD-96, pages 220-227, November 1996.
Suyama et al. (Suyama, hereafter) propose their own SAT algorithm which is not the Davis-Putnam approach. In the Suyama algorithm, each variable in the SAT formula always has some assigned value. The Suyama algorithm proceeds by transitioning from one completely defined set of values to another completely defined set of values. The authors of Suyama propose heuristics to prune the search space, but admit that the number of states visited in their approach can be eight times larger than the basic Davis-Putnam approach. In addition, the Suyama approach requires a max calculator and a complex rule checker, making it very hardware resource intensive.
The above-identified proposal of Abramovici et al. (Abramovici, hereafter) also is not an implementation of the Davis-Putnam SAT algorithm. The Abramovici proposal basically is an implementation of a PODEM-based algorithm in reconfigurable hardware. A PODEM-based algorithm assumes that a satisfying assignment for the entire CNF formula can be found by assigning values to a predefined subset of variables in the formula. For more information on this type of algorithm, see the following document which is hereby incorporated by reference for its useful background information:
This has direct application in the SAT problem generated in the ATPG domain since the circuit under test has well-defined primary inputs and outputs, and since the test vector must be applied at the primary inputs with the result being observed at a primary output. The Abramovici proposal therefore cannot handle a generic CNF formula directly.
Another disadvantage of PODEM (and, thus, Abramovici) is that, even though the number of variables in the SAT decision tree is reduced, there is not necessarily a reduction in the number of states visited during the search. The capturing of relationships between internal variables in Davis-Putnam's efficient data structures has been shown to reduce the state space visited and to reduce the run time significantly over PODEM.
Another disadvantage of the Abramovici proposal is the hardware requirements. These requirements include (i) separate circuits for forward and backward implication, each one a few times larger than the original circuit, (ii) a complex control circuit with 2n inputs, 2n outputs, and 3 n-bit registers, where n is the number of primary inputs, (iii) a very large stack n wide and n deep, (iv) and two copies of the entire original circuit, in order to generate a test for a fault. Although the authors of the Abramovici proposal indicate that the size of the stack potentially can be reduced, such a reduction comes with the expense of significantly increased encoding and decoding circuitry. Thus, the Abramovici proposal is disadvantageous in that the hardware requirements are very great. If a large circuit is tested, this strains the current chip integration or logic emulation limits. Thus, the hardware cost of keeping two circuit copies, in addition to stacks and other control structures, is great.
Most software for SAT solving today is based on the Davis-Putnam algorithm. Recent software implementations of the Davis-Putnam algorithm have enhanced it in various ways while maintaining the same basic flow. To learn more about the enhancements, see the following, each of which is incorporated by reference for its useful background information:
The contribution of the GRASP work is notable since it applies non-chronological backtracking and dynamic clause addition to prune the search space further. The above-identified documents relating to the enhancements to the Davis-Putnam algorithm are directed to software implementations. There is a need for the implementation of such enhancements in reconfigurable hardware, but no prior efforts have successfully achieved the complex flow control required. The control flow associated with non-chronological backtracking is very complex. To the best of the inventors' knowledge, neither the Suyama nor the Abramovici proposal has actually been implemented on a hardware platform at all, and only simulation results have thus far been presented.